Abstract: In Software Engineering, There is much technique to testing. They are Unit testing, Design testing, Code testing …It depends on Development model of a project, the testing maybe before or after. In Viet Nam, the testing for program verification is almost by manually. This thing conducts many shortcoming or overload with big project. Although, there is many try to improve. Such as: present the requirement by XML or looking for many different approaches. But there is no an approach to test become engineering by automatically. From that requirement, it needs a program verification of software interface. There is a tool for testing on the computer by automatically. With this thing, they can save much money, time, and effort. Project is created with two concrete works. One of many importance things is choose a tool that is powerful enough to solve the counter examples. In this project, I choose the Altarica language as that tool. And so, it must be created the input data from XML that Altarica can readable. This operation must be implemented by a parser. To this time, there are two functions Deadlock and Live that are implemented by successfully. And they are used for test run. In the future, there is more function that will develop for maximum support to design.

Keywords: sModel-Based Verification, Model Checking, Altarica for Model Checking, Testing, Formal Design